Proof of proveit.physics.quantum.QPE._psi_t_formula theorem¶

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, c, k, m, n, t, P, defaults, Function
from proveit.linear_algebra import ScalarMult, TensorProd, VecSpaces
from proveit.logic import Equals, InSet
from proveit.numbers import (
        zero, one, two, i, e, pi, Add, Sum, Exp, Less, LessEq, Mult, frac, Neg, subtract)
from proveit.numbers import Complex, Interval, Natural
from proveit.numbers.number_sets.natural_numbers import fold_forall_natural_pos
from proveit.physics.quantum import Ket, NumKet
from proveit.physics.quantum.QPE import _phase, _phase_is_real, _psi_t_def

%proving _psi_t_formula

Keep the $2$ in $2 \pi i$ from combining with powers of $2$:

Exp.change_simplification_directives(factor_numeric_rational=True)

# the induction theorem for positive naturals
fold_forall_natural_pos

# instantiate the induction theorem
induction_inst = fold_forall_natural_pos.instantiate(
    {Function(P,t):_psi_t_formula.instance_expr, m:t, n:t})

Base Case¶

VecSpaces.default_field=Complex
defaults.assumptions = _psi_t_formula.all_conditions()

base_case = induction_inst.antecedent.operands[0]

We have $|\psi_{t}\rangle$ defined as a tensor product (the result of the first phase of the quantum circuit, and the LHS of Nielsen & Chuang's identity 5.20 on pg 222):

_psi_t_def

_psi_t_as_tensor_prod = _psi_t_def.instantiate()

For $\psi'_{1}$, we prove a useful equality then instantiate the psi_t_def with $t=1$:

psi_1_def = _psi_t_def.instantiate({t:one})

Then show that the summation formula also gives the same qbit result

sum_0_to_1 = base_case.rhs

sum_0_to_1_processed_01 = sum_0_to_1.inner_expr().operands[1].partitioning_first()

# finish off the Base Case
base_case_jdgmt = sum_0_to_1_processed_01.sub_left_side_into(psi_1_def)

Inductive Step¶

inductive_step = induction_inst.antecedent.operands[1]

defaults.assumptions = defaults.assumptions + inductive_step.conditions.entries

First, partition the summation: $\sum_{k=0}^{2^{t+1}-1} e^{2\pi i \varphi k} |k\rangle_{t+1} = \sum_{k=0}^{2^{t}-1} e^{2\pi i \varphi k} |k\rangle_{t+1} + \sum_{k=2^{t}}^{2^{t+1}-1} e^{2\pi i \varphi k} |k\rangle_{t+1}$

desired_domain = _psi_t_formula.instance_expr.rhs.scaled.domain

summation_partition_01 = (
    inductive_step.instance_expr.rhs.operands[1]
    .partitioning(desired_domain.upper_bound))

Then shift the second summation of that partition, so that the two summations then have the same index domain:

summation_partition_02 = (summation_partition_01.inner_expr().rhs.
                          operands[1].shift(Neg(Exp(two, t))))

We want to rewrite the summand of that 2nd summation on the rhs now by (1) expanding the exponential term and (2) rewriting the $|k+2^t{\rangle}_{t+1}$ ket as $|1\rangle \otimes |k{\rangle}_t$. This takes a little work.

rhs_2nd_sum = summation_partition_02.rhs.operands[1]

summand_processed_01 = rhs_2nd_sum.summand.inner_expr().operands[0].exponent.distribution(
    4, assumptions=[*defaults.assumptions,
                    rhs_2nd_sum.condition])

summand_processed_02 = (
    summand_processed_01.inner_expr().rhs.operands[0]
    .exponent_separate(
        assumptions=[*defaults.assumptions,
                     InSet(k, Interval(zero, subtract(Exp(two, t), one)))]))

# Avoid recombining these via auto-simplification
defaults.preserved_exprs = set([summand_processed_02.rhs.scalar])

from proveit.physics.quantum.algebra import prepend_num_ket_with_one_ket
prepend_num_ket_with_one_ket

prepend_num_ket_with_one_ket_inst = prepend_num_ket_with_one_ket.instantiate(
        {n: t, k: k},
        assumptions=[*defaults.assumptions, InSet(k, Interval(zero, subtract(Exp(two, t), one)))])

summand_processed_03 = (
    summand_processed_02.inner_expr().rhs.operands[1]
    .substitute(prepend_num_ket_with_one_ket_inst))

# reminder of summation_partition_03
summation_partition_02

summation_partition_04 = (
    summation_partition_02.inner_expr().rhs.operands[1].summand.substitute(
        summand_processed_03))

Also process the summand in the 1st sum on the rhs, converting the ket $|k\rangle_{t+1}$ to the tensor product $|0\rangle \otimes |k\rangle_{t}$:

# pull up the relevant NumKet theorem
from proveit.physics.quantum.algebra import prepend_num_ket_with_zero_ket
prepend_num_ket_with_zero_ket

# instantiate the theorem for our specific case
prepend_num_ket_with_zero_ket_inst = prepend_num_ket_with_zero_ket.instantiate(
        {n: t, k: k},
        assumptions=[*defaults.assumptions, InSet(k, Interval(zero, subtract(Exp(two, t), one)))])

# use our instantiation to substitute
summation_partition_05 = (
    summation_partition_04.inner_expr().rhs.operands[0].summand.scaled.substitute(
    prepend_num_ket_with_zero_ket_inst))

coef = inductive_step.instance_expr.rhs.scalar
summation_partition_06 = summation_partition_05.scalar_mult_both_sides(coef)

# Recall our inductive hypothesis:
inductive_hypothesis = defaults.assumptions[-1]

conclusion_01 = summation_partition_06.inner_expr().rhs.factor(
        inductive_hypothesis.rhs, pull='right', field=Complex)

# use the inductive hypothesis:
conclusion_02 = inductive_hypothesis.sub_left_side_into(conclusion_01)

The RHS of conclusion02 above should be equal to $|\psi{t+1}\rangle$. Let's see how to get there. Ideally we could use the next three cells to show the rhs of the equality in `conclusion_02` is equal to $|\psi_{t+1}\rangle$

# reminder
_psi_t_def

psi_t_plus_one_as_tensor_prod = _psi_t_def.instantiate({t:Add(t, one)})

Now this substitute() step will also manage to pull the scalar coefficients out to the front in the process:

conclusion_03 = conclusion_02.inner_expr().rhs.operands[1].substitute(
        _psi_t_as_tensor_prod)

Now we partition the tensor product expression of $\psi_{t+1}$, so we can eventually show that it is equal to the rhs of conclusion_03.

psi_t_plus_one_as_tensor_prod.rhs

# # we can partition the operands in the psi_{t+1} tensor prod expression
psi_t_plus_one_as_tensor_prod_02 = (
    psi_t_plus_one_as_tensor_prod.inner_expr().rhs.operands[0].split(t))

conclusion_03.inner_expr().rhs.substitute(psi_t_plus_one_as_tensor_prod_02.derive_reversed())

# # recall our earlier instantiation of the induction theorem:
induction_inst

We have proven both pieces of the antecedent (i.e., the base case and inductive case) of the instantiated induction theorem induction_inst, so we can now derive the consequent:

induction_inst.derive_consequent()

_psi_t_formula has been proven.  Now simply execute "%qed".

%qed

proveit.physics.quantum.QPE._psi_t_formula has been proven.

	step type	requirements	statement
0	modus ponens	1, 2	⊢
1	instantiation	3, 4^, 5^, 6^*	⊢
	: , : , :
2	instantiation	7, 8, 9	⊢
	: , :
3	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos
4	instantiation	601, 10, 449	⊢
	: , : , :
5	instantiation	11, 12	⊢
	:
6	instantiation	601, 13, 14	⊢
	: , : , :
7	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
8	instantiation	427, 15, 16	⊢
	: , : , :
9	generalization	17	⊢
10	instantiation	615, 630	⊢
	: , : , :
11	conjecture		⊢
	proveit.physics.quantum.algebra.single_qubit_num_ket
12	instantiation	18, 19, 20	⊢
	:
13	instantiation	615, 126	⊢
	: , : , :
14	instantiation	460, 21	⊢
	: , :
15	instantiation	102, 679, 22, 23^*	⊢
	:
16	instantiation	615, 24	⊢
	: , : , :
17	instantiation	460, 25	, ⊢
	: , :
18	conjecture		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
19	instantiation	682, 26, 28	⊢
	: , : , :
20	instantiation	27, 636, 663, 28	⊢
	: , : , :